Nuprl Lemma : stable__function_equal
9,38
postcript
pdf
A
,
B
:Type,
f
,
g
:(
A
B
). (
x
:
A
. Stable{
f
(
x
) =
g
(
x
)})
Stable{
f
=
g
}
latex
ProofTree
Definitions
,
t
T
,
Stable{
P
}
,
P
Q
,
x
:
A
.
B
(
x
)
,
A
,
False
Lemmas
not
wf
origin
A,B:Type, f,g:(A
B). (x:A. Stable{f(x) = g(x)}) 
Stable{f = g}
A,B:Type, f,g:(AB). (x:A. Stable{f(x) = g(x)}) Stable{f = g}
T Qx:A. B(x)
A